ecl{-}halt{-}kind($x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind($x$;$k$,${\it test}$.inl($k$);$a$,$b$,${\it ha}$,${\it hb}$.${\it hb}$;$a$,$b$,${\it ha}$,${\it hb}$.inr($\cdot$);$a$,$b$,${\it ha}$,${\it hb}$.inr($\cdot$);$a$,${\it ha}$.${\it ha}$;$a$,$m$,${\it ha}$.${\it ha}$;$a$,$m$,${\it ha}$.${\it ha}$;$a$,$l$,${\it ha}$.inr($\cdot$))